Fast Tactic-Based Theorem Proving
Identifieur interne : 000531 ( Main/Exploration ); précédent : 000530; suivant : 000532Fast Tactic-Based Theorem Proving
Auteurs : Jason Hickey [États-Unis] ; Aleksey Nogin [États-Unis]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2000.
Abstract
Abstract: Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and computationally intensive domain-specific proof procedures. The generality of tactic provers has a performance penalty; the speed of proof search lags far behind special-purpose provers. We present a new modular proving architecture that significantly increases the speed of the core logic engine. Our speedup is due to efficient data structures and modularity, which allows parts of the prover to be customized on a domain-specific basis. Our architecture is used in the MetaPRL logical framework, with speedups of more than two orders of magnitude over traditional tactic-based proof search.
Url:
DOI: 10.1007/3-540-44659-1_16
Affiliations:
Links toward previous steps (curation, corpus...)
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Fast Tactic-Based Theorem Proving</title><author><name sortKey="Hickey, Jason" sort="Hickey, Jason" uniqKey="Hickey J" first="Jason" last="Hickey">Jason Hickey</name></author><author><name sortKey="Nogin, Aleksey" sort="Nogin, Aleksey" uniqKey="Nogin A" first="Aleksey" last="Nogin">Aleksey Nogin</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:467A6C15061B1DAD835355E8B57C0166A68DCD02</idno><date when="2000" year="2000">2000</date><idno type="doi">10.1007/3-540-44659-1_16</idno><idno type="url">https://api.istex.fr/document/467A6C15061B1DAD835355E8B57C0166A68DCD02/fulltext/pdf</idno><idno type="wicri:Area/Main/Corpus">000404</idno><idno type="wicri:Area/Main/Curation">000404</idno><idno type="wicri:Area/Main/Exploration">000531</idno><idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Exploration">000531</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Fast Tactic-Based Theorem Proving</title><author><name sortKey="Hickey, Jason" sort="Hickey, Jason" uniqKey="Hickey J" first="Jason" last="Hickey">Jason Hickey</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><placeName><region type="state">Californie</region></placeName><wicri:cityArea>Department of Computer Science, Caltech 256-80, 91125, Pasadena</wicri:cityArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author><author><name sortKey="Nogin, Aleksey" sort="Nogin, Aleksey" uniqKey="Nogin A" first="Aleksey" last="Nogin">Aleksey Nogin</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><placeName><region type="state">État de New York</region></placeName><wicri:cityArea>Department of Computer Science, Cornell University, 14853, Ithaca</wicri:cityArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2000</date></imprint><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">467A6C15061B1DAD835355E8B57C0166A68DCD02</idno><idno type="DOI">10.1007/3-540-44659-1_16</idno><idno type="ChapterID">16</idno><idno type="ChapterID">Chap16</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage to implement both general-purpose reasoning and computationally intensive domain-specific proof procedures. The generality of tactic provers has a performance penalty; the speed of proof search lags far behind special-purpose provers. We present a new modular proving architecture that significantly increases the speed of the core logic engine. Our speedup is due to efficient data structures and modularity, which allows parts of the prover to be customized on a domain-specific basis. Our architecture is used in the MetaPRL logical framework, with speedups of more than two orders of magnitude over traditional tactic-based proof search.</div></front></TEI><affiliations><list><country><li>États-Unis</li></country><region><li>Californie</li><li>État de New York</li></region></list><tree><country name="États-Unis"><region name="Californie"><name sortKey="Hickey, Jason" sort="Hickey, Jason" uniqKey="Hickey J" first="Jason" last="Hickey">Jason Hickey</name></region><name sortKey="Hickey, Jason" sort="Hickey, Jason" uniqKey="Hickey J" first="Jason" last="Hickey">Jason Hickey</name><name sortKey="Nogin, Aleksey" sort="Nogin, Aleksey" uniqKey="Nogin A" first="Aleksey" last="Nogin">Aleksey Nogin</name><name sortKey="Nogin, Aleksey" sort="Nogin, Aleksey" uniqKey="Nogin A" first="Aleksey" last="Nogin">Aleksey Nogin</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Amerique/explor/CaltechV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000531 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000531 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Amerique
|area= CaltechV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:467A6C15061B1DAD835355E8B57C0166A68DCD02
|texte= Fast Tactic-Based Theorem Proving
}}
| This area was generated with Dilib version V0.6.32. |  |